Problem:
 1(q0(1(x1))) -> 0(1(q1(x1)))
 1(q0(0(x1))) -> 0(0(q1(x1)))
 1(q1(1(x1))) -> 1(1(q1(x1)))
 1(q1(0(x1))) -> 1(0(q1(x1)))
 0(q1(x1)) -> q2(1(x1))
 1(q2(x1)) -> q2(1(x1))
 0(q2(x1)) -> 0(q0(x1))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {5,4}
   transitions:
    01(21) -> 22*
    q01(30) -> 31*
    q01(20) -> 21*
    q01(28) -> 29*
    q21(7) -> 8*
    11(14) -> 15*
    11(16) -> 17*
    11(6) -> 7*
    10(2) -> 4*
    10(1) -> 4*
    10(3) -> 4*
    q00(2) -> 1*
    q00(1) -> 1*
    q00(3) -> 1*
    00(2) -> 5*
    00(1) -> 5*
    00(3) -> 5*
    q10(2) -> 2*
    q10(1) -> 2*
    q10(3) -> 2*
    q20(2) -> 3*
    q20(1) -> 3*
    q20(3) -> 3*
    1 -> 28,14
    2 -> 20,6
    3 -> 30,16
    8 -> 17,7,4,5
    15 -> 7*
    17 -> 7*
    22 -> 5*
    29 -> 21*
    31 -> 21*
  problem:
   
  Qed